<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Interrupts | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/Tutorials/">
              <span property="name"><b>Tutorials</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">Interrupts</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    

<div class="sidebar">
  <ul class="nav nav-sidebar tutorial-sidebar">
    <li class="nav-section">Getting started</li>
      <li><a href="/Tutorials/">Overview</a></li>
      <li><a href="/Tutorials/pathways">Tutorial pathways</a></li>
    <li class="nav-section">seL4</li>
      <li><a href="/Tutorials/setting-up">Setting up your machine</a></li>
      <li><a href="/Tutorials/get-the-tutorials">Getting the tutorials</a></li>
      <li><a href="/Tutorials/hello-world">Hello world</a></li>
      <li><a href="/Tutorials/capabilities">Capabilities</a></li>
      <li><a href="/Tutorials/untyped">Untyped</a></li>
      <li><a href="/Tutorials/mapping">Mapping</a></li>
      <li><a href="/Tutorials/threads">Threads</a></li>
      <li><a href="/Tutorials/ipc">IPC</a></li>
      <li><a href="/Tutorials/notifications">Notifications</a></li>
      <li><a href="/Tutorials/interrupts">Interrupts</a></li>
      <li><a href="/Tutorials/fault-handlers">Fault handling</a></li>
      <li><a href="/Tutorials/mcs">MCS extensions</a></li>
    <li class="nav-section">C Libraries</li>
      <li><a href="/Tutorials/libraries-1">Initialisation &amp; threading</a></li>
      <li><a href="/Tutorials/libraries-2">IPC</a></li>
      <li><a href="/Tutorials/libraries-3">Processes &amp; Elf loading</a></li>
      <li><a href="/Tutorials/libraries-4">Timer</a></li>
    <li class="nav-section">Microkit</li>
      <li><a href="https://trustworthy.systems/projects/microkit/tutorial/">Tutorial</a></li>
    <li class="nav-section">CAmkES</li>
      <li><a href="/Tutorials/hello-camkes-0">Hello CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-1">Introduction to CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-2">Events in CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-timer">CAmkES timer tutorial</a></li>
      <li><a href="/Tutorials/camkes-vm-linux">CAmkES VM</a></li>
      <li><a href="/Tutorials/camkes-vm-crossvm">CAmkES cross-VM connectors</a></li>
    <li class="nav-section">Rust</li>
      <li><a href="https://github.com/seL4/rust-sel4">GitHub</a></li>
    <li class="nav-section">Resources</li>
      <li><a href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">seL4 Manual</a></li>
      <li><a href="/projects/sel4/api-doc.html">seL4 API reference</a></li>
      <li><a href="/Tutorials/how-to">How to: a quick solutions guide</a></li>
      <li><a href="/projects/sel4-tutorials/debugging-guide">Debugging guide</a></li>
      <li><a href="/Resources#contact">Help contacts</a></li>
  </ul>
</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">

    
<!--
  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)

  SPDX-License-Identifier: BSD-2-Clause
-->

<h1 id="interrupts">Interrupts</h1>
<p>This tutorial covers seL4 interrupts.</p>

<p>You will learn:</p>
<ol>
  <li>The purpose of the IRQControl capability.</li>
  <li>How to obtain capabilities for specific interrupts.</li>
  <li>How to handle interrupts and their relation with notification objects.</li>
</ol>

<h2 id="prerequisites">Prerequisites</h2>

<ol>
  <li><a href="/Tutorials/setting-up">Set up your machine</a></li>
  <li><a href="/Tutorials/notifications">Notifications tutorial</a></li>
</ol>

<h1 id="initialising">Initialising</h1>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--tut</span> interrupts
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>interrupts_build
ninja
</code></pre></div></div>

<details>
  <summary><em>Hint:</em> tutorial solutions</summary>
  <p><br />
All tutorials come with complete solutions. To get solutions run:</p>

  <div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--solution</span> <span class="nt">--tut</span> interrupts
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>interrupts_build
ninja
</code></pre></div>  </div>

  <p>Answers are also available in drop down menus under each section.</p>
</details>

<h2 id="capdl-loader">CapDL Loader</h2>

<p>This tutorial uses the <em>capDL loader</em>, a root task which allocates statically
 configured objects and capabilities.</p>

<details>
  <summary>Get CapDL</summary>
  <p>The capDL loader parses
a static description of the system and the relevant ELF binaries.
It is primarily used in <a href="https://docs.sel4.systems/CAmkES/">Camkes</a> projects
but we also use it in the tutorials to reduce redundant code.
The program that you construct will end up with its own CSpace and VSpace, which are separate
from the root task, meaning CSlots like <code class="language-plaintext highlighter-rouge">seL4_CapInitThreadVSpace</code> have no meaning
in applications loaded by the capDL loader.
<br />
More information about CapDL projects can be found <a href="https://docs.sel4.systems/CapDL.html">here</a>.
<br />
For this tutorial clone the <a href="https://github.com/sel4/capdl">CapDL repo</a>. This can be added in a directory that is adjacent to the tutorials-manifest directory.</p>
</details>

<h2 id="background">Background</h2>

<h3 id="irqcontrol">IRQControl</h3>

<p>The root task is given a single capability from which capabilities to all irq numbers
in the system can be derived, <code class="language-plaintext highlighter-rouge">seL4_CapIRQControl</code>. This capability can be moved between CSpaces
and CSlots but cannot be duplicated. Revoking this capability results in all access to all
irq capabilities being removed.</p>

<h3 id="irqhandlers">IRQHandlers</h3>

<p>IRQHandler capabilities give access to a single irq and are standard seL4 capabilities: they
<em>can</em> be moved and duplicated according to system policy. IRQHandlers are obtained by
invoking the IRQControl capability, with architecture specific parameters. Below is an
example of obtaining an IRQHandler.</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>// Get a capability <span class="k">for </span>irq number 7 and place it <span class="k">in </span>cslot 10 <span class="k">in </span>a single-level cspace.
error <span class="o">=</span> seL4_IRQControl_Get<span class="o">(</span>seL4_IRQControl, 7, cspace_root, 10, seL4_WordBits<span class="o">)</span><span class="p">;</span>
</code></pre></div></div>

<p>There are a variety of different invocations to obtain irq capabilities which are hardware
dependent, including:</p>

<ul>
  <li><a href="https://docs.sel4.systems/ApiDoc.html#get-io-apic"><code class="language-plaintext highlighter-rouge">seL4_IRQControl_GetIOAPIC</code></a> (x86)</li>
  <li><a href="https://docs.sel4.systems/ApiDoc.html#get-msi"><code class="language-plaintext highlighter-rouge">seL4_IRQControl_GetMSI</code></a> (x86)</li>
  <li><a href="https://docs.sel4.systems/ApiDoc.html#gettrigger"><code class="language-plaintext highlighter-rouge">seL4_IRQControl_GetTrigger</code></a> (ARM)</li>
</ul>

<h3 id="receiving-interrupts">Receiving interrupts</h3>

<p>Interrupts are received by registering a capability to a notification object
with the IRQHandler capability for that irq, as follows:</p>
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>seL4_IRQHandler_SetNotification<span class="o">(</span>irq_handler, notification<span class="o">)</span><span class="p">;</span>
</code></pre></div></div>

<p>On success, this call will result in signals being delivered to the notification object when
an interrupt occurs. To handle multiple interrupts on the same notification object, you
can set different badges on the notification capabilities bound to each IRQHandler.
 When an interrupt arrives,
the badge of the notification object bound to that IRQHandler is bitwise orred with the data
word in the notification object.
Recall the badging technique for differentiating signals from the
 <a href="/Tutorials/notifications">notification tutorial</a>.</p>

<p>Interrupts can be polled for using <code class="language-plaintext highlighter-rouge">seL4_Poll</code> or waited for using <code class="language-plaintext highlighter-rouge">seL4_Wait</code>. Either system
call results in the data word of the notification object being delivered as the badge of the
message, and the data word cleared.</p>

<p><a href="https://docs.sel4.systems/ApiDoc.html#clear"><code class="language-plaintext highlighter-rouge">seL4_IRQHandler_Clear</code></a> can be used to unbind
the notification from an IRQHandler.</p>

<h3 id="handling-interrupts">Handling interrupts</h3>

<p>Once an interrupt is received and processed by the software, you can unmask the interrupt
using <a href="https://docs.sel4.systems/ApiDoc.html#ack"><code class="language-plaintext highlighter-rouge">seL4_IRQHandler_Ack</code></a> on the IRQHandler.
seL4 will not deliver any further interrupts after an IRQ is raised until that IRQHandler
has been acked.</p>

<h2 id="exercises">Exercises</h2>

<p>In this tutorial you will set up interrupt handling for a provided timer driver
on the zynq7000 ARM platform. This timer driver can be located inside the
<code class="language-plaintext highlighter-rouge">projects/sel4-tutorials/zynq_timer_driver</code> folder from the root of the
projects directory, i.e. where the <code class="language-plaintext highlighter-rouge">.repo</code> folder can be found and where the
initial <code class="language-plaintext highlighter-rouge">repo init</code> command was executed. The tutorial has been set up with two
processes: <code class="language-plaintext highlighter-rouge">timer.c</code>, the timer driver and RPC server, and <code class="language-plaintext highlighter-rouge">client.c</code>, which
makes a single request.</p>

<p>On successful initialisation of the tutorial, you will see the following:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>timer client: hey hey hey
timer: got a message from 61 to sleep 2 seconds
&lt;&lt;seL4(CPU 0) [decodeInvocation/530 T0xe8265600 "tcb_timer" @84e4]: Attempted to invoke a null cap #9.&gt;&gt;
main@timer.c:78 [Cond failed: error]
	Failed to ack irq
</code></pre></div></div>

<p>The timer driver we are using emits an interrupt in the <code class="language-plaintext highlighter-rouge">TTC0_TIMER1_IRQ</code> number.</p>

<h3 id="invoke-irq-control">Invoke IRQ control</h3>

<p><strong>Exercise</strong> Invoke <code class="language-plaintext highlighter-rouge">irq_control</code>, which contains the <code class="language-plaintext highlighter-rouge">seL4_IRQControl</code> capability,
the place the <code class="language-plaintext highlighter-rouge">IRQHandler</code> capability for <code class="language-plaintext highlighter-rouge">TTC0_TIMER1_IRQ</code> into the <code class="language-plaintext highlighter-rouge">irq_handler</code> CSlot.</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    /* TODO invoke irq_control to put the interrupt for TTC0_TIMER1_IRQ in
       cslot irq_handler (depth is seL4_WordBits) */

</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* put the interrupt handle for TTC0_TIMER1_IRQ in the irq_handler cslot */</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_IRQControl_Get</span><span class="p">(</span><span class="n">irq_control</span><span class="p">,</span> <span class="n">TTC0_TIMER1_IRQ</span><span class="p">,</span> <span class="n">cnode</span><span class="p">,</span> <span class="n">irq_handler</span><span class="p">,</span> <span class="n">seL4_WordBits</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to get irq capability"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>On success, you should see the following output, without the error message that occurred earlier,
as the irq_handle capability is now valid:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Undelivered IRQ: 42
</code></pre></div></div>

<p>This is a warning message from the kernel that an IRQ was recieved for irq number 42, but no
notification capability is set to sent a signal to.</p>

<h3 id="set-ntfn">Set NTFN</h3>
<p><strong>Exercise</strong> Now set the notification capability (<code class="language-plaintext highlighter-rouge">ntfn</code>) by invoking the irq handler.</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>     /* TODO set ntfn as the notification for irq_handler */

</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="cm">/* set ntfn as the notification for irq_handler */</span>
    <span class="n">error</span> <span class="o">=</span>  <span class="n">seL4_IRQHandler_SetNotification</span><span class="p">(</span><span class="n">irq_handler</span><span class="p">,</span> <span class="n">ntfn</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to set notification"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>Now the output will be:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Tick
</code></pre></div></div>

<p>Only one interrupt is delivered, as the interrupt has not been acknowledged. The timer driver is
programmed to emit an interrupt every millisecond, so we need to count 2000 interrupts
before replying to the client.</p>

<h3 id="acknowledge-an-interrupt">Acknowledge an interrupt</h3>

<p><strong>Exercise</strong> Acknowledge the interrupt after handling it in the timer driver.</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>        /* TODO ack the interrupt */

</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>        <span class="cm">/* ack the interrupt */</span>
        <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_IRQHandler_Ack</span><span class="p">(</span><span class="n">irq_handler</span><span class="p">);</span>
        <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to ack irq"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>Now the timer interrupts continue to come in, and the reply is delivered to the client.</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>timer client wakes up
</code></pre></div></div>

<p>That’s it for this tutorial.</p>



<p style="text-align: right;">

      Next: <a href="/Tutorials/fault-handlers">Fault handling</a>
</p>

<hr>
    <p><em>Tutorial included from <a href="https://github.com/sel4/sel4-tutorials/blob/master/tutorials/interrupts/interrupts.md">github repo</a> <a href="https://github.com/sel4/sel4-tutorials/edit/master/tutorials/interrupts/interrupts.md">edit</a></em></p>
  </div>

  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#prerequisites">Prerequisites</a></li>
<li class="toc-entry toc-h2"><a href="#capdl-loader">CapDL Loader</a></li>
<li class="toc-entry toc-h2"><a href="#background">Background</a>
<ul>
<li class="toc-entry toc-h3"><a href="#irqcontrol">IRQControl</a></li>
<li class="toc-entry toc-h3"><a href="#irqhandlers">IRQHandlers</a></li>
<li class="toc-entry toc-h3"><a href="#receiving-interrupts">Receiving interrupts</a></li>
<li class="toc-entry toc-h3"><a href="#handling-interrupts">Handling interrupts</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#exercises">Exercises</a>
<ul>
<li class="toc-entry toc-h3"><a href="#invoke-irq-control">Invoke IRQ control</a></li>
<li class="toc-entry toc-h3"><a href="#set-ntfn">Set NTFN</a></li>
<li class="toc-entry toc-h3"><a href="#acknowledge-an-interrupt">Acknowledge an interrupt</a></li>
</ul>
</li>
</ul>
</div>

  
</div>
<script src="/assets/js/toggle-markdown.js"></script>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Jan 6 18:52:01 2025 +1100 df31e5ccb8
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/Tutorials/interrupts.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/Tutorials/interrupts.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
